00100	                                                            NIC 13550
00200	
00300	                         Stanford University
00400	                           7 January 1973
00405	
00500	
00600	           THE STANFORD ARTIFICIAL INTELLIGENCE LABORATORY
00700	
00800		Since  the  last  meeting  of  this  group,  the  work of the
00900	Stanford  Artificial  Intelligence  Laboratory   has   included   the
01000	following:
01100	
01200	
01300	VISION AND ROBOTICS
01400	
01500		Our  work  in  robotics  has  continued  to  shift  from  the
01600	artificial  blocks  world to more natural environments. The remaining
01700	block-oriented  research  is  concerned  with  issues   like   visual
01800	feedback[Gill   72]   and   problem-directed  perception  which  have
01900	immediate generalization to  complex  scenes.  There  has  also  been
02000	significant  progress  in  low level vision [Moorer,Pingle] operators
02100	which apply quite generally.
02200	
02300		A great deal of work has  been  applied  to  natural  outdoor
02400	scenes.  Programs  have  been completed for texture [Bajcsy 72],color
02500	[Thomas,Binford] and depth by correlation  [Nevatia,  Quam].  Several
02600	approaches  to  scene  organization  are  being  actively  pursued by
02700	Baumgert,  Yakimovsky,  and  Quam.  Considerable  progress  has  been
02800	achieved  in the repesentation and perception of curved objects [Agin
02900	72] using the laser ranging system.
03000	
03100		The major advance of te year has  come  in  arm  control[Paul
03200	72].  Previous  work has been extended and we are now able to control
03300	with touch, force, free joints, and load compensation.  This  advance
03400	has led us to begin work on a practical assembly device. This applied
03500	project also makes use of much of our recent progress in  vision  and
03600	problem solving.
03700	
03800		There  have  also  been  significant  advances in the support
03900	hardware  and  software.  A  second  arm  and  a  second  camera,each
04000	incorporating    techincal    improvements   have   been   installed.
04100	Considerable effort has been devoted to the design of  new  equipment
04200	for vision, buffering, force and touch sensing and arm control. These
04300	should lead to considerable performance  improvments  in  the  coming
04400	year.
04500	
04600		The  staff  has published a number of papers and organized or
04700	participated  in  many  meetings.  Four  doctoral  dissertations   in
04800	robotics  were  completed and a film describing some of this work was
04900	produced and circulated.
05000	
05100	
05200	MATHEMATICAL THEORY OF COMPUTATION
05300	
05400		During the last year, active work in mathematical  theory  of
05500	computation  was  carried  on  by  Robin  Milner,  Richard Weyhrauch,
05600	Shigeru Igarashi, David Luckham, John McCarthy, Ralph  London,  Zohar
05700	Manna,  Whitfield  Diffie,  and  a number of graduate students in the
05800	Computer Science Department. Some of the most significant  activities
05900	were continued development of the Logic of Computable Functions proof
06000	checker by Milner and Weyhrauch  and  the  First  Order  Logic  proof
06100	checker  by  Whitfield Diffie, the provision of a larger theorem base
06200	in LCF by Malcolm Newey, reformulation of the Scott theory  in  first
06300	order  logic  and  set  theory  by  Igarashi and McCarthy, a study of
06400	definability in LCF by Milner in LCF, a program for the generation of
06500	verification conditions for the Pascal language by Igarashi, Luckham,
06600	and Manna, and Cadiou's thesis on the properties of call-by-value and
06700	call-by-name in evaluating recursively defined functions.
06800	
06900		There  have  turned  out to be more theoretical problems than
07000	were anticipated that have to  be  solved  before  formal  proofs  of
07100	correctness will become a serious competitor of debugging for getting
07200	correct programs. Nevertheless, we are now in a position  to  try  to
07300	formally  prove  the  correctness of two small compilers that produce
07400	PDP-10 machine code from LISP.  Informal proofs of their  correctness
07500	were given earlier by London.
07700	
07800	
07900	REPRESENTATION THEORY
08000	
08100		John   McCarthy   has   established  (at  least  to  his  own
08200	satisfaction) the utility of set theory  in  first  order  logic  for
08300	expressing  causal  laws,  the laws that give the effects of actions,
08400	and sentences telling who knows what and where information is  to  be
08500	obtained.  The system also uses a formalization of LISP S-expressions
08600	in order to do the metamathematics required  to  express  information
08700	about knowledge and belief.
08800	
08900	
09000	SPEECH
09100	
09200		Thosar and Samuel are experimenting with a small system  that
09300	applies   signature   table   learning  to  the  problem  of  phoneme
09400	identification.  They have tested it with a set of 54 words  recorded
09500	by  Ken  Stevens  and  used  earlier  by Gold, Bobrow, Klatt, Vicens,
09600	Erman, and Reddy.  The results are encouraging, though there is  more
09700	work to be done before it can be embedded in a system.
09800	
09900	
10000	HIGH SPEED PROCESSOR
10100	
10200		The logical design of the instruction preparation and  memory
10300	boxes  is  complete  and the drawings are in the computer.  The logic
10400	has been partitioned into circuit boards for these boxes.  The  logic
10500	of  the instruction execution box is almost complete.  More than half
10600	of the printed circuit boards for the machine are laid out ready  for
10700	fabrication,  and  a  start  has  been  made on the wire-wrap boards.
10800	Arrangements have been made with all the suppliers, and  test  boards
10900	for  the  wire-wrap  part  of  the  machine have been made.  Tests to
11000	verify the electrical design of the machine have been  made  and  the
11100	software   support   for  the  automatic  production  of  the  wiring
11200	instructions are almost complete.
11300	
11400	
11500	THEOREM PROVING
11600	
11700		Dr. David Luckham and John Allen have  continued  their  work
11800	with  their  resolution  theorem  prover,  increasing  its  speed and
11900	applying it to more mathematical examples.  They have made it  easier
12000	to  use by giving it a mathematical language pre-processor, and Jorge
12100	Morales has used it to prove a number of  results  announced  in  the
12200	Bulletin  of  the  American Mathematical Society, some of them before
12300	the announcer had completely worked out proofs.
12400	
12500	
12600	NATURAL LANGUAGE
12700	
12800		The Laboratory's work on natural languages and  psychological
12900	modelling  is  largely supported by other funds.  ARPA supported work
13000	includes a small but functioning  semantics  based  natural  language
13100	translation program.
13200	
13300	
13400	LANGUAGES, TIME-SHARING, AND MISCELLANEOUS
13500	
13600		The  Algol  based  SAIL language has been extended to provide
13700	for multi-processing, backtracking, and pattern  matching.   The  new
13800	features  have met wide acceptance at Stanford and elsewhere.  A new,
13900	modern, version of LISP called LISP70 has been under development  for
14000	about a year.
14100	
14200		A  program  that reads the Associated Press A-wire that gives
14300	national and international news and classifies the stories  has  been
14400	put  into  our  system.   A  user  can find news stories according to
14500	Boolean combinations of keywords and  can  select  the  stories  that
14600	interest him.  This program is used about 1000 times a month, half at
14700	Stanford and half over the network.  We consider it  a  demonstration
14800	that  useful  information  services can be provided with a minimum of
14900	programming work and that they don't require great sophistication  to
15000	be useful.  Further activities in this direction are planned.
15100	
15200		McCarthy  has  studied  the  problem  of storage, display and
15300	printing of documents in the network and has concluded that the  next
15400	step  should  be  to  documents  in  arbitrary  character  sets.  The
15500	technology is ready for it.
15600	
15700		The time-sharing system now supports an average of 40 jobs at
15800	a time during the day and is fairly heavily loaded during most of the
15900	night as well.  We are expecting some relief from the  completion  of
16000	the high speed processor.